package b2bpl;

import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.List;

import b2bpl.bpl.transformation.IBPLTransformator;
import b2bpl.bpl.transformation.LoopTransformator;
import b2bpl.bytecode.DefaultSpecificationProvider;
import b2bpl.bytecode.ISpecificationProvider;
import b2bpl.bytecode.bml.ISpecificationDesugarer;
import b2bpl.bytecode.bml.StandardDesugarer;


/**
 * Simple datastructure containing the settings of the project to translate.
 *
 * A {@code Project} contains the information about the bytecode classes
 * to translate as well as other user configurations such as the set of
 * transformations to apply to the resulting Boogie program and other
 * settings which, to some extent, determine the behavior of the
 * {@link Main compiler}. A convenience method is provided for creating an
 * adequately configured {@code Project} based on a set of supported
 * command line arguments.
 *
 * @see Main
 * @see ISpecificationProvider
 * @see IBPLTransformator
 *
 * @author Ovidio Mallo, Samuel Willimann
 */
public class Project {

  /**
   * The names of the classes to verify. Defaults to the empty set.
   *
   * @see #getProjectTypes()
   */
  private String[] projectTypes = new String[0];

  /**
   * The optional {@link ISpecificationProvider} to be used for the project.
   * Defaults to a minimal {@code DefaultSpecificationProvider}.
   *
   * @see #getSpecificationProvider()
   */
  private ISpecificationProvider specificationProvider = new DefaultSpecificationProvider();

  /**
   * The {@link ISpecificationDesugarer} to be used for BML specifications.
   * Defaults to a {@link StandardDesugarer}.
   *
   * @see #getSpecificationDesugarer()
   */
  private ISpecificationDesugarer specificationDesugarer = new StandardDesugarer();

  /**
   * The set of transformators to apply to the BoogiePL program generated during
   * the translation. Defaults to the empty set.
   *
   * @see #getTransformators()
   */
  private IBPLTransformator[] transformators = new IBPLTransformator[0];

  /**
   * The file to which to output the BoogiePL program generated during the
   * translation in case all the bytecode classes are translated into a single
   * BoogiePL program. Defaults to the string {@code "-"} which represents
   * the standard output.
   *
   * C@see #translateSeparately
   * @see #getOutFile()
   */
  private String outFile = "-";

  /**
   * Whether to translate every bytecode class to a separate BoogiePL program
   * in a separate file. Defaults to {@code false}. If this flag is turned
   * on, the BoogiePL program belonging to a specific bytecode class will be
   * output to a separate file whose name is the class' name followed by the
   * file ending ".bpl" and the outfile eventually set on the project will be
   * ignored.
   *
   * @see #isTranslateSeparately()
   */
  private boolean translateSeparately = false;

  /**
   * Whether the BoogiePL program generated should only check whether the
   * object invariants of the this object have been violated instead of
   * verifying the invariants of all instances of the method's receiver type.
   *
   * @see #isThisInvariantsOnly()
   */
  private boolean thisInvariantsOnly = false;

  /**
   * Whether to explicitly model the control flow in bytecode methods
   * originating from the runtime exceptions thrown by individual bytecode
   * instructions. Defaults to {@code false}, meaning that runtime
   * exceptions are, by default, not modeled in the control flow graph and
   * ruled out by appropriate verification conditions during the program
   * verification.
   *
   * @see #isModelRuntimeExceptions()
   */
  private boolean modelRuntimeExceptions = false;

  /**
   * The maximal <i>magnitude</i> of constants to represent explicitly in the
   * BoogiePL program generated by the translation. This avoids the theorem
   * prover having to deal with very large constants which may have a negative
   * impact on the performance of the verification. Defaults to 100000.
   *
   * @see #getMaxIntConstant()
   */
  private int maxIntConstant = 100000;

  /**
   * If set to {@code true}, logical expressions will be simplified
   * while they are being built. For instance, the expression {@code (false || x)}
   * is simplified to the expression {@code x}.
   *
   * @see #simplifyLogicalExpressions()
   */
  private boolean simplifyLogicalExpressions = false;
  
  /**
   * If set to {@code true}, triggers will be added to the axioms
   * of the background theory (where applicable).
   * 
   * @see #useTriggers()
   */
  private boolean useTriggers = false;
  
  /**
   * If set ti {@code true}, object invariant checks will be included.
   * in the resulting BoogiePL code.
   */
  private boolean performInvariantChecks = false;
  
  /**
   * The root directory used to look for the given classes if they are
   * not found in the Java's class path.
   * 
   * @see #getBaseDirectory = "";
   */
  private String baseDirectory = "";

  /**
   * Creates a new project which is configured according to the set of command
   * line arguments ({@code args}) provided.
   *
   * @param args           The set of command line arguments which will
   *                       determine the configuration of the new project.
   * @param messageWriter  A writer to which help messages about the supported
   *                       command line arguments or possible errors occurred
   *                       while parsing the command line arguments are
   *                       delegated.
   * @return               The new, configured project, or {@code null}
   *                       if some error occurred while parsing the command
   *                       line arguments or if only the help message was
   *                       requested.
   */
  public static Project fromCommandLine(
      String[] args,
      PrintWriter messageWriter) {
    Project project = new Project();
  
//System.out.print("> b2bpl.Main ");
//for (String arg : args) System.out.print(arg + " ");
//System.out.println();
    
    
    List<String> types = new ArrayList<String>();
    List<IBPLTransformator> transformators = new ArrayList<IBPLTransformator>();

    int i = 0;
    while (i < args.length) {
      if ("-h".equals(args[i])) {
        printHelpMessage(messageWriter);
        return null;
      } else if ("-o".equals(args[i])) {
        // An explicit output file has been specified
        project.outFile = args[i + 1];
        i += 2;
      } else if ("-s".equals(args[i])) {
        project.translateSeparately = true;
        i++;
      } else if ("-this".equals(args[i])) {
        // Check invariants in "this" object only
        project.thisInvariantsOnly = true;
        i++;
      } else if ("-l".equals(args[i])) {
        // Turn on loop transformation
        transformators.add(new LoopTransformator());
        i++;
      } else if ("-r".equals(args[i])) {
        // Handle runtime exceptions
        project.modelRuntimeExceptions = true;
        i++;
      } else if ("-c".equals(args[i])) {
        // Set maximum integer constant that is treated as a number
        project.modelRuntimeExceptions = true;
        project.maxIntConstant = Integer.valueOf(args[i + 1]);
        i += 2;
      } else if ("-basedir".equals(args[i])) {
        // Set base directory for classes that are not located in the CLASSPATH
        project.baseDirectory = args[i + 1];
        i += 2;
      } else if ("-sl".equals(args[i])) {
        // Simplify logical expressions, e.g. (false || x) <==> x
        project.simplifyLogicalExpressions = true;
        i++;
      } else if ("-t".equals(args[i])) {
        // Use triggers in axioms
        project.useTriggers = true;
        i++;
      } else if ("-i".equals(args[i])) {
        // Perform object invariant checks
        project.performInvariantChecks = true;
        i++;
      } else {
        if (args[i].endsWith(".class")) {
          args[i] = args[i].substring(0, args[i].lastIndexOf(".class"));
        }
        // TODO(rgrig): Don't NullPointerException when the class can't be loaded
        types.add(args[i].replace('/', '.'));
        i++;
      }
    }

    project.projectTypes   = types.toArray(new String[types.size()]);
    project.transformators = transformators.toArray(new IBPLTransformator[transformators.size()]);

    return project;
  }

  public String[] getProjectTypes() {
    return projectTypes;
  }

  public ISpecificationProvider getSpecificationProvider() {
    return specificationProvider;
  }

  public ISpecificationDesugarer getSpecificationDesugarer() {
    return specificationDesugarer;
  }

  public IBPLTransformator[] getTransformators() {
    return transformators;
  }

  public String getOutFile() {
    return outFile;
  }

  public boolean isTranslateSeparately() {
    return translateSeparately;
  }

  public String getSeparateOutFile(int typeIndex) {
    return projectTypes[typeIndex] + ".bpl";
  }

  public boolean isThisInvariantsOnly() {
    return thisInvariantsOnly;
  }

  public boolean isModelRuntimeExceptions() {
    return modelRuntimeExceptions;
  }

  public int getMaxIntConstant() {
    return maxIntConstant;
  }
  
  public String getBaseDirectory() {
    return baseDirectory;
  }
  
  public boolean simplifyLogicalExpressions() {
    return simplifyLogicalExpressions;
  }
  
  public boolean useTriggers() {
    return useTriggers;
  }
  
  public boolean performInvariantChecks() {
    return performInvariantChecks;
  }

  /**
   * Prints the help message describing the command line arguments supported
   * along with their semantics.
   *
   * @param messageWriter  The writer to direct the help message to.
   */
  private static void printHelpMessage(PrintWriter messageWriter) {
    messageWriter.write("Usage: java b2bpl.Main [<options>] [<files>]\n");
    messageWriter.write('\n');
    messageWriter.write("<options>:\n");
    messageWriter.write("  -h              Print this help message.\n");
    messageWriter.write("  -o <outfile>    The file to which to write the BoogiePL program.\n");
    messageWriter.write("  -s              Translate every class into a separate file.\n");
    messageWriter.write("  -t              Adds triggers to the axioms (where applicable).\n");
    messageWriter.write("  -i              Includes invariant checks.\n");
    messageWriter.write("  -sl             Removes redundancy from logical formulas.\n");
    messageWriter.write("  -this           Verify the object invariants of the this object only.\n");
    messageWriter.write("  -l              Perform a sound elimination of loops in the BoogiePL program.\n");
    messageWriter.write("  -r              Model runtime exceptions of bytecode instructions (instead of ruling them out).\n");
    messageWriter.write("  -c <constant>   The magnitude of the largest integer constant to represent explicitly.\n");
    messageWriter.write("  -basedir <path> Base directory where class files are located (if different from CLASSPATH)");
    messageWriter.write('\n');
    messageWriter.write("<files>:\n");
    messageWriter.write("  The class files or type names of the classes to verify (drawn from the CLASSPATH).\n");
    messageWriter.flush();
  }
}
